導出可能性 (⊢)

導出可能性Γ⊢φは、仮定集合Γから推論規則を有限回適用してφを構成できることを表す構文上の関係である。意味的帰結Γ⊨φとは、証明の存在とモデルでの真偽を分ける。

仕組みと確認

証明木・適用規則・未解消仮定を記録し、各ステップが規則に適合することを検査する。自動化では、証明器が出した証明オブジェクトを独立に検証する。

限界と注意点

導出できないことは直ちに偽を意味しない。体系が不完全、前提が不足、または探索が終了していない可能性を区別する。